%invariante estanAlMenosUnDia:
(\forall x \selec Salidas(h))(\forall i \selec ingresosDe(x,h))\neg(\exists j \selec salidasDe(x,h))snd(i)==snd(j)
